environ
vocabularies HIDDEN, ORDERS_2, SUBSET_1, YELLOW_0, XXREAL_0, EQREL_1, LATTICE3, LATTICES, SETFAM_1, XBOOLE_0, RELAT_2, WAYBEL_0, TARSKI, STRUCT_0, ORDINAL2, REWRITE1, YELLOW_1, ZFMISC_1, RELAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, LATTICE3, YELLOW_0, DOMAIN_1, STRUCT_0, ORDERS_2, YELLOW_1, WAYBEL_0, YELLOW_3;
definitions LATTICE3, TARSKI, WAYBEL_0, XBOOLE_0;
theorems LATTICE3, ORDERS_2, TARSKI, WAYBEL_0, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, XBOOLE_0;
schemes ;
registrations STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2;
constructors HIDDEN, DOMAIN_1, LATTICE3, YELLOW_1, YELLOW_3, WAYBEL_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions LATTICE3, TARSKI, WAYBEL_0;
Lm2:
now for L being non empty RelStr
for x, y, z being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}
let L be non
empty RelStr ;
for x, y, z being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}let x,
y,
z be
Element of
L;
{ (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}thus
{ (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}
verum
proof
thus
{ (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "\/" y),(x "\/" z)}
XBOOLE_0:def 10 {(x "\/" y),(x "\/" z)} c= { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
proof
let q be
object ;
TARSKI:def 3 ( not q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "\/" y),(x "\/" z)} )
assume
q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
;
q in {(x "\/" y),(x "\/" z)}
then consider u,
v being
Element of
L such that A1:
q = u "\/" v
and A2:
u in {x}
and A3:
v in {y,z}
;
A4:
(
v = y or
v = z )
by A3, TARSKI:def 2;
u = x
by A2, TARSKI:def 1;
hence
q in {(x "\/" y),(x "\/" z)}
by A1, A4, TARSKI:def 2;
verum
end;
let q be
object ;
TARSKI:def 3 ( not q in {(x "\/" y),(x "\/" z)} or q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } )
A5:
z in {y,z}
by TARSKI:def 2;
assume
q in {(x "\/" y),(x "\/" z)}
;
q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
then A6:
(
q = x "\/" y or
q = x "\/" z )
by TARSKI:def 2;
(
x in {x} &
y in {y,z} )
by TARSKI:def 1, TARSKI:def 2;
hence
q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
by A6, A5;
verum
end;
end;
Lm4:
now for L being non empty RelStr
for x, y, z being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}
let L be non
empty RelStr ;
for x, y, z being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}let x,
y,
z be
Element of
L;
{ (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}thus
{ (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}
verum
proof
thus
{ (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "/\" y),(x "/\" z)}
XBOOLE_0:def 10 {(x "/\" y),(x "/\" z)} c= { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
proof
let q be
object ;
TARSKI:def 3 ( not q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "/\" y),(x "/\" z)} )
assume
q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
;
q in {(x "/\" y),(x "/\" z)}
then consider u,
v being
Element of
L such that A1:
q = u "/\" v
and A2:
u in {x}
and A3:
v in {y,z}
;
A4:
(
v = y or
v = z )
by A3, TARSKI:def 2;
u = x
by A2, TARSKI:def 1;
hence
q in {(x "/\" y),(x "/\" z)}
by A1, A4, TARSKI:def 2;
verum
end;
let q be
object ;
TARSKI:def 3 ( not q in {(x "/\" y),(x "/\" z)} or q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } )
A5:
z in {y,z}
by TARSKI:def 2;
assume
q in {(x "/\" y),(x "/\" z)}
;
q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
then A6:
(
q = x "/\" y or
q = x "/\" z )
by TARSKI:def 2;
(
x in {x} &
y in {y,z} )
by TARSKI:def 1, TARSKI:def 2;
hence
q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }
by A6, A5;
verum
end;
end;