defpred S₁[ FormalConcept of C, FormalConcept of C, set ] means ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( $3 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of $1 \/ the Extent of $2)) & A = the Intent of $1 /\ the Intent of $2 );
A1: for CP1, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S₁[CP1,CP2,CP]

proof

let CP1, CP2 be Element of B-carrier C; :: thesis: ex CP being Element of B-carrier C st S₁[CP1,CP2,CP]
set O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2));
set A = the Intent of CP1 /\ the Intent of CP2;
reconsider O' = the Extent of CP1 \/ the Extent of CP2 as Subset of the carrier of C ;
A2: (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) = the Intent of CP1 /\ the Intent of CP2

proof

(ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) = (ObjectDerivation C) . O' by Th7
.= ((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2) by Th16
.= the Intent of CP1 /\ ((ObjectDerivation C) . the Extent of CP2) by Def13
.= the Intent of CP1 /\ the Intent of CP2 by Def13 ;
hence (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))) = the Intent of CP1 /\ the Intent of CP2 ; :: thesis: verum

end;

then A3: (AttributeDerivation C) . (the Intent of CP1 /\ the Intent of CP2) = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) by Th7;
then A4: not ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))),(the Intent of CP1 /\ the Intent of CP2) #) is empty by A2, Lm1;
set CP = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))),(the Intent of CP1 /\ the Intent of CP2) #);
ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2))),(the Intent of CP1 /\ the Intent of CP2) #) in { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } by A2, A3, A4;
hence ex CP being Element of B-carrier C st S₁[CP1,CP2,CP] ; :: thesis: verum

end;

consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that
A5: for CP1, CP2 being Element of B-carrier C holds S₁[CP1,CP2,f . CP1,CP2] from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (B-carrier C) ;
A6: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . CP1,CP2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 )

proof

let CP1, CP2 be strict FormalConcept of C; :: thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . CP1,CP2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 )
( CP1 is Element of B-carrier C & CP2 is Element of B-carrier C ) by Th35;
hence ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . CP1,CP2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) by A5; :: thesis: verum

end;

take f ; :: thesis: for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . CP1,CP2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 )
thus for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . CP1,CP2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) by A6; :: thesis: verum