let B be non empty set ; :: thesis: ( ( for a being Element of B holds varcl a = a ) implies varcl (meet B) = meet B )
set A = meet B;
assume A1: for a being Element of B holds varcl a = a ; :: thesis: varcl (meet B) = meet B

now :: thesis: ( meet B c= meet B & ( for x, y being set st [x,y] in meet B holds
x c= meet B ) )

thus meet B c= meet B ; :: thesis: for x, y being set st [x,y] in meet B holds
x c= meet B
let x, y be set ; :: thesis: ( [x,y] in meet B implies x c= meet B )
assume A2: [x,y] in meet B ; :: thesis: x c= meet B

now :: thesis: for Y being set st Y in B holds
x c= Y

let Y be set ; :: thesis: ( Y in B implies x c= Y )
assume A3: Y in B ; :: thesis: x c= Y
then A4: [x,y] in Y by A2, SETFAM_1:def 1;
Y = varcl Y by A1, A3;
hence x c= Y by A4, Def1; :: thesis: verum

end;

hence x c= meet B by SETFAM_1:5; :: thesis: verum

end;

hence varcl (meet B) c= meet B by Def1; :: according to XBOOLE_0:def 10 :: thesis: meet B c= varcl (meet B)
thus meet B c= varcl (meet B) by Def1; :: thesis: verum