defpred S1[ 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 S1[CP1,CP2,CP]
proof
let CP1,
CP2 be
Element of
B-carrier C;
ex CP being Element of B-carrier C st S1[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
S1[
CP1,
CP2,
CP]
;
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 S1[CP1,CP2,f . (CP1,CP2)]
from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (B-carrier C) ;
take
f
; 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)) )
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)) )
; verum