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 & X c= Y 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 & X c= Y holds
FinMeetCl B = {Y} \/ (FinMeetCl A)
let B be Subset-Family of Y; :: thesis: ( A = B & X in A & X c= Y implies FinMeetCl B = {Y} \/ (FinMeetCl A) )
assume A1: ( A = B & X in A & X c= Y ) ; :: 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 set ; :: 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
A2: ( y c= B & y is finite & x = Intersect y ) by CANTOR_1:def 4;
reconsider z = y as Subset-Family of X by A1, A2, 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 A2, SETFAM_1:def 10;
then x in {Y} by TARSKI:def 1;
hence x in {Y} \/ (FinMeetCl A) by XBOOLE_0:def 3; :: thesis: verum

end;

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

then ( Intersect y = meet y & Intersect z = meet y ) by SETFAM_1:def 10;
then x in FinMeetCl A by A1, A2, CANTOR_1:def 4;
hence x in {Y} \/ (FinMeetCl A) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {Y} \/ (FinMeetCl A) or x in FinMeetCl B )
assume A3: x in {Y} \/ (FinMeetCl A) ; :: thesis: x in FinMeetCl B
consider E being empty Subset-Family of Y;

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

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

then ( x = Y & Intersect E = Y & E c= B ) by SETFAM_1:def 10, TARSKI:def 1, XBOOLE_1:2;
hence x in FinMeetCl B by CANTOR_1:def 4; :: 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
A4: ( y c= A & x = Intersect y ) by A1, Th14;
reconsider z = y as Subset-Family of Y by A1, A4, XBOOLE_1:1;
reconsider z = z as Subset-Family of Y ;
x = meet z by A4, SETFAM_1:def 10
.= Intersect z by SETFAM_1:def 10 ;
hence x in FinMeetCl B by A1, A4, CANTOR_1:def 4; :: thesis: verum

end;

end;