let a, b be set ; :: thesis: ( a in Fin X & b in Fin X implies ex c being set st
( a \/ b c= c & c in Fin X ) )
assume A1: ( a in Fin X & b in Fin X ) ; :: thesis: ex c being set st
( a \/ b c= c & c in Fin X )
take c = a \/ b; :: thesis: ( a \/ b c= c & c in Fin X )
thus a \/ b c= c ; :: thesis: c in Fin X
( a c= X & b c= X ) by A1, FINSUB_1:def 5;
then a \/ b c= X by XBOOLE_1:8;
hence c in Fin X by A1, FINSUB_1:def 5; :: thesis: verum

reconsider c = {} as set ;
let a, b be set ; :: thesis: ( a in Fin X & b in Fin X implies ex c being set st
( c c= a /\ b & c in Fin X ) )
assume that
a in Fin X and
b in Fin X ; :: thesis: ex c being set st
( c c= a /\ b & c in Fin X )
take c = c; :: thesis: ( c c= a /\ b & c in Fin X )
thus c c= a /\ b ; :: thesis: c in Fin X
thus c in Fin X by FINSUB_1:7; :: thesis: verum