let X be set ; :: thesis: for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
Intersect A = Intersect B
let A, B be Subset-Family of X; :: thesis: ( ( A = B \/ {X} or B = A \ {X} ) implies Intersect A = Intersect B )
assume A1: ( A = B \/ {X} or B = A \ {X} ) ; :: thesis: Intersect A = Intersect B
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Intersect B c= Intersect A
let x be object ; :: thesis: ( x in Intersect A implies x in Intersect B )
assume A2: x in Intersect A ; :: thesis: x in Intersect B
now :: thesis: for y being set st y in B holds
x in y
let y be set ; :: thesis: ( y in B implies x in y )
assume y in B ; :: thesis: x in y
then y in A by A1, XBOOLE_0:def 3, XBOOLE_0:def 5;
hence x in y by A2, SETFAM_1:43; :: thesis: verum
end;
hence x in Intersect B by A2, SETFAM_1:43; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersect B or x in Intersect A )
assume A3: x in Intersect B ; :: thesis: x in Intersect A
now :: thesis: for y being set st y in A holds
x in y
let y be set ; :: thesis: ( y in A implies x in y )
assume y in A ; :: thesis: x in y
then ( ( y in B & not y in {X} ) or y in {X} ) by A1, XBOOLE_0:def 3, XBOOLE_0:def 5;
then ( y in B or y = X ) by TARSKI:def 1;
hence x in y by A3, SETFAM_1:43; :: thesis: verum
end;
hence x in Intersect A by A3, SETFAM_1:43; :: thesis: verum