let C be FormalContext; :: thesis: ( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )
set G = rng (gamma C);
thus
rng (gamma C) is supremum-dense
:: thesis: rng (delta C) is infimum-dense proof
let a be
Element of
(ConceptLattice C);
:: according to LATTICE6:def 13 :: thesis: ex b1 being Element of bool (rng (gamma C)) st a = "\/" b1,(ConceptLattice C)
A1:
"\/" { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,
(ConceptLattice C) = a @
by Th9;
A2:
{ ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } c= rng (gamma C)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } or x in rng (gamma C) )
assume
x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) }
;
:: thesis: x in rng (gamma C)
then consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A3:
(
x = ConceptStr(#
O,
A #) & ex
o being
Object of
C st
(
o in the
Extent of
(a @ ) &
O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) &
A = (ObjectDerivation C) . {o} ) )
;
consider o being
Object of
C such that A4:
(
o in the
Extent of
(a @ ) &
O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) &
A = (ObjectDerivation C) . {o} )
by A3;
A5:
dom (gamma C) = the
carrier of
C
by FUNCT_2:def 1;
consider y being
Element of
(ConceptLattice C) such that A6:
(gamma C) . o = y
;
consider O' being
Subset of the
carrier of
C,
A' being
Subset of the
carrier' of
C such that A7:
(
y = ConceptStr(#
O',
A' #) &
O' = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) &
A' = (ObjectDerivation C) . {o} )
by A6, Def4;
thus
x in rng (gamma C)
by A3, A4, A5, A6, A7, FUNCT_1:def 5;
:: thesis: verum
end;
a = a @
by CONLAT_1:def 24;
hence
ex
b1 being
Element of
bool (rng (gamma C)) st
a = "\/" b1,
(ConceptLattice C)
by A1, A2;
:: thesis: verum
end;
set G = rng (delta C);
let b be Element of (ConceptLattice C); :: according to LATTICE6:def 14 :: thesis: ex b1 being Element of bool (rng (delta C)) st b = "/\" b1,(ConceptLattice C)
A8:
"/\" { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C) = b @
by Th10;
A9:
{ ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } c= rng (delta C)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } or x in rng (delta C) )
assume
x in { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) }
;
:: thesis: x in rng (delta C)
then consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A10:
(
x = ConceptStr(#
O,
A #) & ex
a being
Attribute of
C st
(
a in the
Intent of
(b @ ) &
O = (AttributeDerivation C) . {a} &
A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) )
;
consider a being
Attribute of
C such that A11:
(
a in the
Intent of
(b @ ) &
O = (AttributeDerivation C) . {a} &
A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )
by A10;
A12:
dom (delta C) = the
carrier' of
C
by FUNCT_2:def 1;
consider y being
Element of
(ConceptLattice C) such that A13:
(delta C) . a = y
;
consider O' being
Subset of the
carrier of
C,
A' being
Subset of the
carrier' of
C such that A14:
(
y = ConceptStr(#
O',
A' #) &
O' = (AttributeDerivation C) . {a} &
A' = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )
by A13, Def5;
thus
x in rng (delta C)
by A10, A11, A12, A13, A14, FUNCT_1:def 5;
:: thesis: verum
end;
b = b @
by CONLAT_1:def 24;
hence
ex b1 being Element of bool (rng (delta C)) st b = "/\" b1,(ConceptLattice C)
by A8, A9; :: thesis: verum