let X be set ; :: thesis: for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
FinMeetCl A = FinMeetCl B
let A, B be Subset-Family of X; :: thesis: ( ( A = B \/ {X} or B = A \ {X} ) implies FinMeetCl A = FinMeetCl B )
assume A1: ( A = B \/ {X} or B = A \ {X} ) ; :: thesis: FinMeetCl A = FinMeetCl B
X in FinMeetCl B by CANTOR_1:8;
then ( {X} c= FinMeetCl B & B c= FinMeetCl B & (A \ {X}) \/ {X} = A \/ {X} ) by CANTOR_1:4, XBOOLE_1:39, ZFMISC_1:37;
then ( A c= B \/ {X} & B \/ {X} c= FinMeetCl B ) by A1, XBOOLE_1:7, XBOOLE_1:8;
then A c= FinMeetCl B by XBOOLE_1:1;
then FinMeetCl A c= FinMeetCl (FinMeetCl B) by CANTOR_1:16;
hence FinMeetCl A c= FinMeetCl B by CANTOR_1:13; :: according to XBOOLE_0:def 10 :: thesis: FinMeetCl B c= FinMeetCl A
B c= A by A1, XBOOLE_1:7, XBOOLE_1:36;
hence FinMeetCl B c= FinMeetCl A by CANTOR_1:16; :: thesis: verum