let X, Y be set ; :: thesis: for A being Subset-Family of X
for B being Subset-Family of Y st A = B & X in A holds
FinMeetCl B = {Y} \/ (FinMeetCl A)
let A be Subset-Family of X; :: thesis: for B being Subset-Family of Y st A = B & X in A holds
FinMeetCl B = {Y} \/ (FinMeetCl A)
let B be Subset-Family of Y; :: thesis: ( A = B & X in A implies FinMeetCl B = {Y} \/ (FinMeetCl A) )
assume that
A1: A = B and
A2: X in A ; :: thesis: FinMeetCl B = {Y} \/ (FinMeetCl A)
thus FinMeetCl B c= {Y} \/ (FinMeetCl A) :: according to XBOOLE_0:def 10 :: thesis: {Y} \/ (FinMeetCl A) c= FinMeetCl B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl B or x in {Y} \/ (FinMeetCl A) )
assume x in FinMeetCl B ; :: thesis: x in {Y} \/ (FinMeetCl A)
then consider y being Subset-Family of Y such that
A3: y c= B and
A4: y is finite and
A5: x = Intersect y by CANTOR_1:def 3;
reconsider z = y as Subset-Family of X by A1, A3, XBOOLE_1:1;
reconsider z = z as Subset-Family of X ;

per cases ( y = {} or y <> {} ) ;

suppose y = {} ; :: thesis: x in {Y} \/ (FinMeetCl A)

then x = Y by A5, SETFAM_1:def 9;
then x in {Y} by TARSKI:def 1;
hence x in {Y} \/ (FinMeetCl A) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A6: y <> {} ; :: thesis: x in {Y} \/ (FinMeetCl A)

then A7: Intersect y = meet y by SETFAM_1:def 9;
Intersect z = meet y by A6, SETFAM_1:def 9;
then x in FinMeetCl A by A1, A3, A4, A5, A7, CANTOR_1:def 3;
hence x in {Y} \/ (FinMeetCl A) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {Y} \/ (FinMeetCl A) or x in FinMeetCl B )
assume A8: x in {Y} \/ (FinMeetCl A) ; :: thesis: x in FinMeetCl B

per cases ( x in {Y} or x in FinMeetCl A ) by A8, XBOOLE_0:def 3;

suppose x in {Y} ; :: thesis: x in FinMeetCl B

then A9: x = Y by TARSKI:def 1;
A10: Intersect ({} (bool Y)) = Y by SETFAM_1:def 9;
{} (bool Y) c= B ;
hence x in FinMeetCl B by A9, A10, CANTOR_1:def 3; :: thesis: verum

end;

suppose x in FinMeetCl A ; :: thesis: x in FinMeetCl B

then consider y being non empty finite Subset-Family of X such that
A11: y c= A and
A12: x = Intersect y by A2, Th14;
reconsider z = y as Subset-Family of Y by A1, A11, XBOOLE_1:1;
reconsider z = z as Subset-Family of Y ;
x = meet z by A12, SETFAM_1:def 9
.= Intersect z by SETFAM_1:def 9 ;
hence x in FinMeetCl B by A1, A11, CANTOR_1:def 3; :: thesis: verum

end;

end;