let u be object ; :: thesis: ( ( v = TRUE & w = TRUE implies ( u = v '&' w iff u = TRUE ) ) & ( ( not v = TRUE or not w = TRUE ) implies ( u = v '&' w iff u = FALSE ) ) )
thus ( v = TRUE & w = TRUE implies ( u = v '&' w iff u = TRUE ) ) ; :: thesis: ( ( not v = TRUE or not w = TRUE ) implies ( u = v '&' w iff u = FALSE ) )
assume ( v <> TRUE or w <> TRUE ) ; :: thesis: ( u = v '&' w iff u = FALSE )
then ( v = FALSE or w = FALSE ) by XBOOLEAN:def 3;
hence ( u = v '&' w iff u = FALSE ) ; :: thesis: verum