let I be set ; :: thesis: for sf, sg, sh being Subset-Family of I st sh = sf \/ sg holds
Intersect sh = (Intersect sf) /\ (Intersect sg)
let sf, sg, sh be Subset-Family of I; :: thesis: ( sh = sf \/ sg implies Intersect sh = (Intersect sf) /\ (Intersect sg) )
assume A1: sh = sf \/ sg ; :: thesis: Intersect sh = (Intersect sf) /\ (Intersect sg)
per cases ( ( sf = {} & sg = {} ) or ( sf <> {} & sg = {} ) or ( sf = {} & sg <> {} ) or ( sf <> {} & sg <> {} ) ) ;
suppose ( sf = {} & sg = {} ) ; :: thesis: Intersect sh = (Intersect sf) /\ (Intersect sg)
hence Intersect sh = (Intersect sf) /\ (Intersect sg) by A1; :: thesis: verum
end;
suppose A2: ( sf <> {} & sg = {} ) ; :: thesis: Intersect sh = (Intersect sf) /\ (Intersect sg)
hence Intersect sh = meet sf by A1, SETFAM_1:def 9
.= (meet sf) /\ I by XBOOLE_1:28
.= (Intersect sf) /\ I by A2, SETFAM_1:def 9
.= (Intersect sf) /\ (Intersect sg) by A2, SETFAM_1:def 9 ;
:: thesis: verum
end;
suppose A3: ( sf = {} & sg <> {} ) ; :: thesis: Intersect sh = (Intersect sf) /\ (Intersect sg)
hence Intersect sh = meet sg by A1, SETFAM_1:def 9
.= I /\ (meet sg) by XBOOLE_1:28
.= I /\ (Intersect sg) by A3, SETFAM_1:def 9
.= (Intersect sf) /\ (Intersect sg) by A3, SETFAM_1:def 9 ;
:: thesis: verum
end;
suppose A4: ( sf <> {} & sg <> {} ) ; :: thesis: Intersect sh = (Intersect sf) /\ (Intersect sg)
then A5: Intersect sg = meet sg by SETFAM_1:def 9;
( Intersect sh = meet sh & Intersect sf = meet sf ) by A1, A4, SETFAM_1:def 9;
hence Intersect sh = (Intersect sf) /\ (Intersect sg) by A1, A4, A5, SETFAM_1:9; :: thesis: verum
end;
end;