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 A2: {X} c= FinMeetCl B by ZFMISC_1:31;
A3: B c= FinMeetCl B by CANTOR_1:4;
(A \ {X}) \/ {X} = A \/ {X} by XBOOLE_1:39;
then A4: A c= B \/ {X} by A1, XBOOLE_1:7;
B \/ {X} c= FinMeetCl B by A2, A3, XBOOLE_1:8;
then A c= FinMeetCl B by A4;
then FinMeetCl A c= FinMeetCl (FinMeetCl B) by CANTOR_1:14;
hence FinMeetCl A c= FinMeetCl B by CANTOR_1:11; :: according to XBOOLE_0:def 10 :: thesis: FinMeetCl B c= FinMeetCl A
thus FinMeetCl B c= FinMeetCl A by A1, CANTOR_1:14, XBOOLE_1:7, XBOOLE_1:36; :: thesis: verum