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 O9 = the Extent of CP1 \/ the Extent of CP2 as Subset of the carrier of C ;
set CP = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #);
A2: (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) = (ObjectDerivation C) . O9 by Th7
.= ((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2) by Th15
.= the Intent of CP1 /\ ((ObjectDerivation C) . the Extent of CP2) by Def9
.= the Intent of CP1 /\ the Intent of CP2 by Def9 ;
then ( (AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2) = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & 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 Lm1, Th7;
then 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;
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
A3: 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) ;
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 )
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 Th31;
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 A3; :: thesis: verum

end;

hence 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 ) ; :: thesis: verum