let X be set ; :: thesis: for A, B being Subset-Family of X st A c= B holds
FinMeetCl A c= FinMeetCl B
let A, B be Subset-Family of X; :: thesis: ( A c= B implies FinMeetCl A c= FinMeetCl B )
assume A1: A c= B ; :: thesis: FinMeetCl A c= FinMeetCl B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl A or x in FinMeetCl B )
assume A2: x in FinMeetCl A ; :: thesis: x in FinMeetCl B
then reconsider x = x as Subset of X ;
consider y being Subset-Family of X such that
A3: y c= A and
A4: ( y is finite & x = Intersect y ) by A2, Def4;
y c= B by A1, A3, XBOOLE_1:1;
hence x in FinMeetCl B by A4, Def4; :: thesis: verum