let T be Ternary_Boolean_Algebra; :: thesis: for x being Element of T holds JoinTBA (T,x) absorbs MeetTBA (T,x)

let x be Element of T; :: thesis: JoinTBA (T,x) absorbs MeetTBA (T,x)

set ff = JoinTBA (T,x);

set gg = MeetTBA (T,x);

for a, b being Element of the carrier of T holds (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a

let x be Element of T; :: thesis: JoinTBA (T,x) absorbs MeetTBA (T,x)

set ff = JoinTBA (T,x);

set gg = MeetTBA (T,x);

for a, b being Element of the carrier of T holds (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a

proof

hence
JoinTBA (T,x) absorbs MeetTBA (T,x)
by LATTICE2:def 1; :: thesis: verum
let a, b be Element of the carrier of T; :: thesis: (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a

(JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = (JoinTBA (T,x)) . (a,(Tern (a,(x `),b))) by MeetDef

.= Tern (a,x,(Tern (a,(x `),b))) by JoinDef

.= Tern ((Tern (a,x,(x `))),x,(Tern (a,(x `),b))) by TRADef

.= Tern ((Tern (a,(x `),x)),x,(Tern (a,(x `),b))) by Th36a

.= Tern (a,(x `),(Tern (x,x,b))) by TDis

.= Tern (a,(x `),(Tern (x,b,x))) by Th36a

.= Tern (a,(x `),x) by Th32

.= Tern (a,x,(x `)) by Th36a

.= a by TRADef ;

hence (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a ; :: thesis: verum

end;(JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = (JoinTBA (T,x)) . (a,(Tern (a,(x `),b))) by MeetDef

.= Tern (a,x,(Tern (a,(x `),b))) by JoinDef

.= Tern ((Tern (a,x,(x `))),x,(Tern (a,(x `),b))) by TRADef

.= Tern ((Tern (a,(x `),x)),x,(Tern (a,(x `),b))) by Th36a

.= Tern (a,(x `),(Tern (x,x,b))) by TDis

.= Tern (a,(x `),(Tern (x,b,x))) by Th36a

.= Tern (a,(x `),x) by Th32

.= Tern (a,x,(x `)) by Th36a

.= a by TRADef ;

hence (JoinTBA (T,x)) . (a,((MeetTBA (T,x)) . (a,b))) = a ; :: thesis: verum