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 = the Extent of $1 /\ the Extent of $2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( 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 = the Extent of CP1 /\ the Extent of CP2;
set A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2));
reconsider A9 = the Intent of CP1 \/ the Intent of CP2 as Subset of the carrier' of C ;
set CP = ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #);
A2: (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) = (AttributeDerivation C) . A9 by Th8
.= ((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . the Intent of CP2) by Th16
.= the Extent of CP1 /\ ((AttributeDerivation C) . the Intent of CP2) by Def9
.= the Extent of CP1 /\ the Extent of CP2 by Def9 ;
then A3: (ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2) = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) by Th7;
then not ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #) is empty by Lm1;
then ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( 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;
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
A4: 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 = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( 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 = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( 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 = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( 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 = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) by A4; :: 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 = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) ; :: thesis: verum